e'e.P(e') == e':es-E(es). es-le(es; e; e')  P(e') 

latex

---

clarification:

alle-ge(es;e;e'.P(e')) == e':es-E(es). es-le(es; e; e')  P(e') 

latex

Definitions	x:A. B(x), es-E(es), P  Q, es-le(es; e; e')
FDL editor aliases	alle-ge